\begin{tabbing}
$\forall$${\it es}$:ES, $x$, ${\it free}$:Id, $n$:$\mathbb{N}$, $e$:E.
\\[0ex]@loc($e$)($x$:Id)
\\[0ex]$\Rightarrow$ ($\neg$(($x$ after $e$) = ($x$ when $e$) $\in$ Id))
\\[0ex]$\Rightarrow$ (0 $<$ $n$)
\\[0ex]$\Rightarrow$ ($n$ $\leq$ round($e$))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex](${\it e'}$ $\leq$loc $e$  \& rank(${\it e'}$) = $<$$n$, 0$>$ $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$) \& ($\neg$(($x$ after ${\it e'}$) = ($x$ when ${\it e'}$) $\in$ Id))))
\-
\end{tabbing}